YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [D](x1) = x1 + 3*x1^2 [t]() = 0 [1]() = 0 [constant]() = 0 [0]() = 0 [+](x1, x2) = x1 + x2 [*](x1, x2) = 1 + x1 + x2 [-](x1, x2) = x1 + x2 This order satisfies the following ordering constraints. [D(t())] = >= = [1()] [D(constant())] = >= = [0()] [D(+(x, y))] = x + y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 >= x + 3*x^2 + y + 3*y^2 = [+(D(x), D(y))] [D(*(x, y))] = 4 + 7*x + 7*y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 > 2 + 2*y + 2*x + 3*x^2 + 3*y^2 = [+(*(y, D(x)), *(x, D(y)))] [D(-(x, y))] = x + y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 >= x + 3*x^2 + y + 3*y^2 = [-(D(x), D(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) , D(-(x, y)) -> -(D(x), D(y)) } Weak Trs: { D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { D(-(x, y)) -> -(D(x), D(y)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [D](x1) = x1 + 3*x1^2 [t]() = 0 [1]() = 0 [constant]() = 0 [0]() = 0 [+](x1, x2) = x1 + x2 [*](x1, x2) = 1 + x1 + x2 [-](x1, x2) = 1 + x1 + x2 This order satisfies the following ordering constraints. [D(t())] = >= = [1()] [D(constant())] = >= = [0()] [D(+(x, y))] = x + y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 >= x + 3*x^2 + y + 3*y^2 = [+(D(x), D(y))] [D(*(x, y))] = 4 + 7*x + 7*y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 > 2 + 2*y + 2*x + 3*x^2 + 3*y^2 = [+(*(y, D(x)), *(x, D(y)))] [D(-(x, y))] = 4 + 7*x + 7*y + 3*x^2 + 3*x*y + 3*y*x + 3*y^2 > 1 + x + 3*x^2 + y + 3*y^2 = [-(D(x), D(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) } Weak Trs: { D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { D(+(x, y)) -> +(D(x), D(y)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [D](x1) = 3*x1 + x1^2 [t]() = 0 [1]() = 0 [constant]() = 0 [0]() = 0 [+](x1, x2) = 1 + x1 + x2 [*](x1, x2) = 1 + x1 + x2 [-](x1, x2) = x1 + x2 This order satisfies the following ordering constraints. [D(t())] = >= = [1()] [D(constant())] = >= = [0()] [D(+(x, y))] = 4 + 5*x + 5*y + x^2 + x*y + y*x + y^2 > 1 + 3*x + x^2 + 3*y + y^2 = [+(D(x), D(y))] [D(*(x, y))] = 4 + 5*x + 5*y + x^2 + x*y + y*x + y^2 > 3 + 4*y + 4*x + x^2 + y^2 = [+(*(y, D(x)), *(x, D(y)))] [D(-(x, y))] = 3*x + 3*y + x^2 + x*y + y*x + y^2 >= 3*x + x^2 + 3*y + y^2 = [-(D(x), D(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { D(t()) -> 1() , D(constant()) -> 0() } Weak Trs: { D(+(x, y)) -> +(D(x), D(y)) , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { D(t()) -> 1() , D(constant()) -> 0() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [D](x1) = 1 + 3*x1 + x1^2 [t]() = 0 [1]() = 0 [constant]() = 0 [0]() = 0 [+](x1, x2) = 1 + x1 + x2 [*](x1, x2) = 1 + x1 + x2 [-](x1, x2) = 1 + x1 + x2 This order satisfies the following ordering constraints. [D(t())] = 1 > = [1()] [D(constant())] = 1 > = [0()] [D(+(x, y))] = 5 + 5*x + 5*y + x^2 + x*y + y*x + y^2 > 3 + 3*x + x^2 + 3*y + y^2 = [+(D(x), D(y))] [D(*(x, y))] = 5 + 5*x + 5*y + x^2 + x*y + y*x + y^2 >= 5 + 4*y + 4*x + x^2 + y^2 = [+(*(y, D(x)), *(x, D(y)))] [D(-(x, y))] = 5 + 5*x + 5*y + x^2 + x*y + y*x + y^2 > 3 + 3*x + x^2 + 3*y + y^2 = [-(D(x), D(y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { D(t()) -> 1() , D(constant()) -> 0() , D(+(x, y)) -> +(D(x), D(y)) , D(*(x, y)) -> +(*(y, D(x)), *(x, D(y))) , D(-(x, y)) -> -(D(x), D(y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))